i, x, y:Id, k:Knd, T, A, B:Type, f:(ABTA).
y = x
 @i: ma-single-effect1(x;A;y;B;k;T;f)  Dsys
 & (D:Dsys.
 & (@i: ma-single-effect1(x;A;y;B;k;T;f)  D
 & ( D 
 & ( realizes es.
 & ( vartype(i;x)  A & vartype(i;y)  B
 & ( & (e:E. loc(e) = i  Id  kind(e) = k  Knd  valtype(e)  T)
 & ( & (e:E.
 & ( & (loc(e) = i  Id
 & ( & ( kind(e) = k  Knd
 & ( & ( (x after e) = f((x when e),y when e,val(e))  A)) 

latex

Definitions

Void, t  T, x:A. B(x), Top, KindDeq, x:A. B(x), P  Q, Knd, {T}, SQType(T), s = t, Prop, s ~ t, left+right, x:AB(x), loc(e), Id, valtype(e), P & Q, E, Dsys, World, FairFifo, Atom$n, Type, <a,b>, False, A, D1  D2, x:AB(x), A & B, PossibleWorld(D;w), isrcv(k), b, destination(l), A/x,y. B(x;y), 1of(t), b, , a = b, P  Q, P  Q, x. t(x), vartype(i;x), Valtype(da;k), s.x, x when e, D realizes es. P(es), State(ds), f(x)?z, Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, Unit, EqDecider(T), ma-single-effect1(x;A;y;B;k;T;f), ES(the_w), kind(e), f(a), x.A(x), x : v, IdDeq, f  g

Lemmas

s-effect-rule, deq wf, subtype rel self, ma-valtype wf, ma-state wf, fpf-join wf, dsys wf, d-sub wf, world wf, fair-fifo wf, possible-world wf, fpf-cap-single-join, fpf-join-cap-sq, fpf-single wf, top wf, fpf-cap-single, fpf-single-dom-sq, eqof eq btrue, id-deq wf, bool cases, eqtt to assert, bool sq, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, bool wf, bnot wf, not wf, assert wf, isrcv wf, es-E wf, es-kind wf, Id wf, es-loc wf, w-es wf, Knd sq, fpf-cap-single1, Knd wf, Kind-deq wf